
% 由于分了多个文件, auctex的索引有点问题，
% 必须得在每个文件中都加入如下语句
% 才可以正确索引figure
% 其他类型则无此要求
% 定义所有的eps文件在 figures 子目录下
\graphicspath{{figures/}}

\chapter{基于事务的层次化形式验证方法}
\label{cha:hierarchy}

% 需要包括的内容: 
%    背景知识简介( Model Checking, SMT, 符号模型检验(SMV) )
%    我的方法(层次化研究方法)
%    初步试验结果及分析
%    结论和将来的工作

\section{形式化验证方法简介}
\label{sec:hierarchy-intro}

一般情况下，形式验证可以分为等价性验证和性质检验。

\subsection{等价性验证}
\label{sec:equal}
% TO-DO: 介绍等价性验证

\subsection{性质检验}
\label{sec:property-checking}
% TO-DO: 介绍性质检验

\subsection{形式验证方法层次}
\label{sec:fv-categories}

{\bf 这里需要介绍TLM层，RT层等概念，顺便把transaction的概念也介绍一下}

% 介绍下形式验证的层次, Gate-Level => RTL => Transaction Level
根据``摩尔定律''，集成电路（Intergrated Chips）上可容纳的晶体管数目，约每隔18个月便会增加一倍，性能也
将提升一倍。因此随着集成电路技术的不断发展，片上系统(System-on-Chips)的复杂度和规模都随之越来越大。
相应的，对相关电子设计的验证工作也面临着很大的挑战。这种情况下，传统的集中在寄存器传输级(RTL)的验证
方法就在验证效率方面显得捉襟见肘：一方面，将大规模的设计在相对底层的寄存器传输级验证需要大量的时间和
精力；另一方面，寄存器传输级的电子设计一般在后期才能够成形以供验证，这就势必提高了修正设计失误的代
价，从而影响了上市时间，严重的甚至会导致整条产品线上市的严重滞后，从而造成巨大的经济损失。因此，业界
目前普遍比较关注将验证层次提高

\section{层次化验证方法}
\label{sec:hierarchy-details}
为了比较清晰地介绍层次化验证方法，我们将在下文中结合具体的验证实例来进行阐释。

\subsection{待验证设计}
\label{sec:hierarchy-duv}

我们选用的待验证设计(DUV, Design under Verification) 是DTL(Device Transaction Level)协议。DTL协议是
由Philips提供的一种用于点对点的同步数据传输协议 \cite{DATE09_Moll}，支持单字节传输和块数据传输，以及
错误信号发射以及子字(subword)操作。除此之外，DTL协议还为特定的应用提供了扩展接
口和信号，比如:

\begin{itemize}
  \item 寻址模式: 为块数据传输所提供的包装、固定以及递减地址。
  \item 二维块操作: 用于操作内存中以二维形式存储的数据。
  \item 安全操作: 标明某个事务是否安全。
  \item 缓冲区管理: 允许组件请求写缓冲区，或者在数据到达目的地后发送通知。
\end{itemize}

基本的DTL协议由24个信号组成，其中6个用于扩展特性，比如说缓冲区管理或者二维数据操
作\cite{Book_Pasricha}。为了描述的简洁起见，我们对原始的基本DTL协议进行了简化。在简化后的协议中，仅保
留字节传输支持，并且不支持任何扩展。这样一来，24个信号中仅有12个需要保留。读/写操作是总线协议中最为重
要的两种操作，因此所保留的12个信号中大多与这两种操作相关，这一点在后文中会进一步详细阐述。

除了简化的工作以外，为了更好地描述层次化验证的思想，我们在原始的DTL协议之上又增加了一层扩展。除了基
本的读写操作之外，我们引入了并行的读/写操作，并为此设计了互斥和同步机制。其具体内容如下:

\begin{extension} \label{extension:multi-read}
当且仅当没有写操作访问同一地址时，多个读操作可以同时进行。
\end{extension}
\begin{extension} \label{extension:multi-write}
当且仅当没有读/写操作访问同一地址时，多个写操作可以同时进行。
\end{extension}


为了支持如上两种扩展，两个信号被添加到原始的信号集中: {\em is\_trans} 标示当前是否有正在进行的事
务；{\em is\_rd} 标示当前正在进行的事务是写操作还是读操作。经过简化和扩展之后，共有14个信号被引入，
并根据其用途划分成四组，具体请参见表~\ref{tab:dtl}。在后文的描述中，我们将改造后的DTL协议称为DTL-S协
议。

\begin{table}[ht]
  \caption{DTL-S协议信号和功能组}
  \label{tab:dtl}
  \centering
  \begin{tabular}{c | c}
   \toprule[1.5pt]
    功能组  & 信号\\ [0.5ex]
    \hline
    命令    & cmd\_valid, cmd\_accept, cmd\_finish\\
    \hline
    写操作  & wr\_valid, wr\_addr, wr\_data, wr\_accept\\
    \hline
    读操作  & rd\_valid, rd\_addr, rd\_data, rd\_accept\\
    \hline
    互斥操作  & is\_trans, is\_rd\\
   \bottomrule[1.5pt]
 \end{tabular}
\end{table}

根据信号的名称，我们可以很自然地理解其功能。比如{\em cmd\_valid}信号用来指示命令是否生效，而{\em
  wr\_addr} 则表示写操作的地址。DTL-S协议的整体工作流程如下: 首先发送命令并在验证后设置其为有效；然
后再根据命令的具体内容进行读/写操作。

\subsection{待验证性质}
\label{sec:hierarchy-puv}
在验证过程中需要关注的性质大致分为两类: 安全性和活性。在介绍这两种待验证性质之前，我们有必要介绍一下
性质的表示方法---时态逻辑(Temporal Logic)。

\subsubsection{性质表示: 时态逻辑}
\label{sec:temporal-logic}
为了形式化地表示待验证的性质，时态逻辑的概念被引入，它是一个形式化的表达式，可以用来表示系统目前所处
状态的性质以及状态迁移序列的性质。按照时间展开的不同结构，时态逻辑可以进一步划分为线性时态逻
辑(Linear Temporal Logic)和分支时态逻辑(Branching Time Logic)。这两者的区别类似于确定性状态机和非确定
性状态机之间的区别: 对于线性时态逻辑(LTL)，每个时刻的未来只有一个时刻可以到达；而对于分支时态逻
辑(BTL)\cite{AASPPL83_Clarke}来说，顾名思义，每个时刻的未来都有多个时刻可以到达。下面我们分别对其进行
介绍。

\paragraph{线性时态逻辑LTL}
\label{sec:ltl}

线性时态逻辑的组成部分包括命题逻辑和时态操作符，其中时态操作符包括四种\cite{Book_Bianjn}:

\begin{itemize}
\item $\mathbf X$ ``次态(next time)''操作符
\item $\mathbf F$ ``最终(eventually)''操作符
\item $\mathbf G$ ``全程(globally)''操作符
\item $\mathbf U$ ``直到(until)''操作符
\end{itemize}

在这四种操作符中，$\mathbf X$，$\mathbf F$，$\mathbf G$为一元操作符，而$\mathbf U$为二元操作符。下面
我们结合具体的例子来说明这四种时态操作符的作用。假设有两种命题$req$和$ack$，其中$req$表示请求，而
$ack$则表示对$req$请求的响应。

\begin{itemize}
\item $\mathbf{X}\ ack$ 请求将会在下一个时刻被响应
\item $\mathbf{F}\ ack$ 请求最终会被响应
\item $\mathbf{G}\ req$ 请求将会一直被保持
\item $p\ \mathbf{U}\ q$ 在响应之前，请求将会一直被保持
\end{itemize}

\paragraph{计算树逻辑CTL}
\label{sec:ctl}

在分支时态逻辑(BTL)中，最常用的是计算树逻辑(Compunational Tree Logic)，它所关注的是在状态迁移中具有
分支路径的时态逻辑。为了支持这个特性，其表示方式相比线性时态逻辑LTL，增加了两个路径量词:

\begin{itemize}
\item $\mathbf A$ 全称量词，用于表示状态迁移中的所有的路径
\item $\mathbf E$ 存在量词，表示所有可选路径中至少存在一条路径
\end{itemize} 

因此，通过结合两种路径量词和四种时态操作符，我们在使用计算树逻辑CTL时，共有8种时态操作符可以使用，分
别是$\mathbf AX$，$\mathbf EX$，$\mathbf AF$，$\mathbf EF$，$\mathbf AG$，$\mathbf EG$，$\mathbf
AU$ 和 $\mathbf EU$。

% TO-DO: 这里还可以对8种时态操作符进行解释

\subsubsection{安全性}
\label{sec:safety}

安全性(Safety)指的是某危险事件永不发生，或者某事件永远满足。比如说，安全性可以用来保证系统的互斥和同
步机制的正确实现，比如说资源的互斥使用。另外也可以用来保证一些特定的性质，比如说请求在响应前必须保持。

用线性时态逻辑LTL举例说明的话, $\mathcal{G} \neg(ack1 \wedge ack2)$表示响应$ack1$和$ack2$是互斥的，不可
能同时发生。$\mathbf{G}\ (req \rightarrow ( req\ \mathbf{U}\ ack))$ 则表示一旦有请求$req$产生，那么
在响应$ack$出现之前，请求$req$必须一直保持。

在本例中，我们需要保证的是DTL-S协议中互斥机制的正确实现，也就是说，扩展~\ref{extension:multi-read}
和扩展~\ref{extension:multi-write} 中所描述的性质必须被满足。比如说，假设在具体的系统实现中，有两个
处理器$p1$和$p2$可以通过总线访问同一块内存，其中采用的总线协议是DTL-S，具体请参加图~\ref{fig:shared_memory}。

\begin{figure}[hl]
\centering
\includegraphics[scale=0.6]{shared_memory}
\caption{共享存储器访问模型}
\label{fig:shared_memory}
\end{figure} 

为了保证互斥操作的正确实现，即不会有多个读写或多个写操作同时访问同一内存地址，我们需要验证DTL-S协议能
够满足公式~\eqref{equ:safety}所示的性质。也就是说，在$p1$和$p2$访存地址相同的情况下，两者只能同时是读操作，否
则根据互斥机制，两个操作不能同时被接受。

\begin{equation} \label{equ:safety}
\begin{split}
\mathbf{G}!&((p1.wr\_addr == p2.wr\_addr\ \&\ p1.wr\_accept\ \&\ p2.wr\_accept)\\
&|\ (p1.wr\_addr == p2.rd\_addr\ \& \ p1.wr\_accept\ \&\ p2.wr\_accept)\\
&|\ (p2.wr\_addr == p1.rd\_addr\ \& \ p2.wr\_accept\ \&\ p1.wr\_accept))
\end{split}
\end{equation}

\subsubsection{活性}
\label{sec:liveness}

活性(Liveness)所关注的是某事件最终必须要发生。比如说对于实际应用中的大部分系统来说，我们希望如果用户
给出请求以后，系统最终能够给与回应，用线性时态逻辑LTL表示的话，就是$\mathbf{G}(req \rightarrow ack)$。

在本例中，我们也需要关注相似的性质，也就是说，DTL-S协议应当能够满足公式~(\ref{equ:liveness})所示的性
质。也就是说，只要有命令被确认为有效，就一定会继而触发读/写命令。

\begin{equation} \label{equ:liveness}
\begin{split}
\mathbf{G}(
&(p1.cmd\_accept \rightarrow p1.wr\_valid\ |\ p1.rd\_valid)\\
&(p2.cmd\_accept \rightarrow p2.wr\_valid\ |\ p2.rd\_valid))
\end{split}
\end{equation}

注意，虽然公式~(\ref{equ:safety})和公式~(\ref{equ:liveness})所示的性质必须经过验证过程来判断是否满
足，但是我们要注意到在高层的验证过程中某些特定的信号，比如说公式~(\ref{equ:safety})中的
$p1.wr\_addr$，会在抽象过程中消失。这样的话，我们有可能需要在进一步验证性质是否成立的时候对抽象后的
模型重新进行细化。这一点我们将在~\ref{sec:hierarchy-method}中进行详细的阐述。


\subsection{层次化验证方法}
\label{sec:hierarchy-method}

寄存器传输级(RTL)的设计由于处于相对底层，不可避免的要引入大量的信号，这在目前日益复杂的电子设计中表现
地尤为明显。这样一来，对寄存器传输级设计的验证问题规模就日益扩大，从而给验证技术带来了不小的难题。

一方面，由于电子设计的规模日趋庞大，基于寄存器传输级的设计的验证工作要耗费大量的时间和精力，这正是基
于事务的设计/验证目前受到广泛关注的原因。事务级(Transaction Level)相对于寄存器传输级(RTL)来说抽象层次
更高，因此待验证模型的规模会大大减少，验证效率则会相应地有很大提高。与此同时也可以将验证工作提前到设
计的相对初期来做，可以更早地发现设计失误并予以解决，从而可以尽可能地避免由于设计失误造成的损失，同时
大大缩短上市时间。

另一方面，在待验证的诸多性质中，如果有一些细粒度的性质，需要设计到具体的信号，显然就不适合在高层做验
证。因此事务级建模TLM以及基于事务的验证方法就不适用于这一类性质，验证的完整性也无法保证。在验证这类
涉及到具体信号的性质时，比较理想的方法则是将待验证设计在寄存器传输级(RTL)建模，然后再进行验证。

综上所述，单一地在寄存器传输级(RTL)和事务级(TL)做验证都各有利弊: 寄存器传输级的验证可以更好地保证验证
的完整性，但验证效率会大打折扣；事务级的验证则恰恰相反。而如果可以将两者结合起来，使其可以互相补充，
则可以在很大程度上同时保证验证的完整性和效率。这正是我们提出层次化验证方法的动机。

简单来说，我们会将待验证性质根据粒度划分为两部分: 粗粒度的性质比较适合于基于事务级的验证，而细粒度的
性质则比较适合于寄存器传输级的验证。在验证之初，我们优先保证验证效率，将原始设计做事务级建模，相应
的，也把待验证性质做响应的形式化表示，然后尽可能多地对所有性质做验证。

但正如之前讲到的，由于关注底层细节，很多性质在高层次无法得到确切的验证结论。比如说对于保证多个进程不

 会同时写同一地址的安全性$P$来说，如果我们在寄存器传输级的模型中可以获取该性质的反例，如$p1$和$p2$同时
写内存地址$0x1000$，那么几乎必然的，我们也可以在事务级获得该性质的反例。这是因为事务级模型和寄存
器传输级模型相比，关注的更为高层和宏观，因此就其表现形式有限状态机来说，事务级模型相当于将寄存器传输
级模型中的相关状态整合成状态组，状态组内部的迁移关系也随之被隐藏。违反安全性$P$的反例中，必定存在两
个进程同时写同一地址的情况，这种情况在寄存器传输级表现为$p1.wr\_addr1$和$p2.wr\_addr2$两个信号取值相
同，而在事务级则表现为$p1$和$p2$同时处于写阶段。而由于模型进行了抽象，对于相关的性质我们也要进行
抽象，这时在事务级出现的两者同时处于写阶段也会被认为是原始性质$P$的反例。反过来，$p1$和$p2$同时
处于写阶段是抽象后性质$P'$的反例，却不一定是原始性质$P$的反例，因为此时虽然两者同时处于写阶段，但操
作地址却未必相同。

总而言之，针对在寄存器传输级模型中对于性质$P$的反例$C$，我们也可以在抽象层次高的事务级模型中找到
相对应的对于性质$P'$的反例。反之则不成立。也就是说，在事务级验证过程中证明满足的性质(即无法找到反
例)，我们认为它在较低抽象层次的寄存器传输级也成立。反之，如果我们在基于事务级的验证过程中发现抽
象后性质$P'$的反例，则需要重新验证该反例是否也存在于寄存器传输级模型以及原始性质$P$。

\begin{figure}[ht]
\centering
\includegraphics[scale=0.6]{hierarchy_verification_flow}
\caption{层次化验证流程}
\label{fig:hierarchy_verification_flow}
\end{figure} 

层次化验证的流程如图~\ref{fig:hierarchy_verification_flow}所示，我们采用定界模型检验的方法，同时借鉴
抽象细化的思想。首先将性质取反，结合事务级模型(TLM)进行验证。如果性质不满足，则说明并没有找到反例，结
束验证过程。否则的话，需要在抽象级别低的寄存器传输级模型中进一步验证。我们将于下文中分三部分对其具体
进行介绍: 抽象与建模、模型检验与细化以及对模型检验的改进。

\subsubsection{抽象与建模}
\label{sec:abstract-model}

近年来关于如何对原始设计进行比较恰当的事务级建模吸引了众多相关研究人员的注意，虽然陆续有相关的方法和
流程问世，但从根本上说，抽象时粒度的选择仍然是一个亟待解决的问题。Cai Lukai 和 Gajski
Daniel\cite{Cai:2003:TLM:944645.944651}介绍了6中不同的事务级建模方法。其类型的划分是以计算和通信的粒
度作为衡量标准，每个标准都分为时钟周期无关 (Un-timed)，近似时钟周期 (Approximate-timed)和时钟周期精
确 (Cycle-Accurate)这三个粒度，具体请参见图~\ref{fig:6_tlm}。在建模过程中，需要根据具体的需求来选取不
同的建模粒度。Moll等人也提出了一种为DTL协议建立总线周期精确(Bus Cycle Accurate)模型的具体方
法\cite{DATE09_Moll}，且在要求时间精度的情况下，该方法建立的总线周期精确(BCA)模型与寄存器传输
级(RTL)模型相比，仍然可以做到在模拟速度上有很大的提升。因此在抽象过程中，我们将会借鉴这种方法，并将在
后文中详细讨论该方法的细节。

\begin{figure}[ht]
\centering
\includegraphics[scale=0.6]{6_tlm}
\caption{6种事务级模型\cite{Cai:2003:TLM:944645.944651}}
\label{fig:6_tlm}
\end{figure} 

在实际的验证过程中，我们并不总是要求待验证模型是时钟周期精确的，而且由于其粒度较细，基于其的验证工作
效率较低，我们在流程开始之初采用时钟周期无关(Un-timed)模型，当且仅当有需要的时候才对模型进行细化。在
编码方面，根据不同的模型，我们选取了TLM 2.0 标准\cite{TLM_Standards}中的不同编码风格: LT
(loosely-timed)风格用于时钟周期无关模型，AT(approximate-timed)风格用于模糊时钟周期模型，而对于需要更
精确复杂度的模型，我们可以利用TLM标准中提供的针对通用负载(generic payload)和阶段(phase)的扩展来实现
\cite{DATE09_Moll}。

% TO-DO: 在介绍模型检验时，要介绍下模型的表示。边老师的书上讲的是用

在建模过程中，有多种形式化模型可供选择，比如说Petri网，CSP(Communication Sequential Process)，有限状
态机 (Finite State Machine)等等。在本文中，我们采用了有限状态机，这是因为在模型检验中，有限状态机是
最为常用的一种形式化模型，因此处理有限状态机的高效模型检验器比较容易找到
\cite{DBLP:conf/cav/CimattiCGGPRST02}。如下是基于事务的时钟周期无关模型的抽象过程:

\begin{enumerate}
\item {\bf 信号分类} 根据信号的功能和属性，它们可以被划分为不同的信号组。并且处于简化分类的目的，部
  分信号可能会被同时划分到不同的组。这一步的最终结果实际上已经表现在表~\ref{tab:dtl}中。
\item {\bf 创建有限状态机:} 为了创建状态机，首先需要通过确定时间点\cite{DATE09_Moll}来找出不同的信号组之
  间的状态变迁关系。但是由于目前所采用的待验证模型是时序无关的，这一步可以省略，直接将信号组转换为相
  关的状态。最终的结果如图~\ref{fig:un-timed}所示。
\item {\bf 事务阶段映射:} 事务阶段可以根据上一步确立的时间点信息来确定，每个有限状态机(FSM)中的状态都
  应该被映射到一个独立的事务阶段中。对于目前采用的时序无关(Un-timed)模型，最终得到的事务阶段与有限状
  态机的状态完全一致: 命令阶段(COMMAND)，写操作阶段(WRITE)，读操作阶段(READ)。
\item {\bf 性质转换:} 如果待验证性质中引入了已经在建模过程中被抽象掉的信号，那么为了正确地基于抽象后
  的模型进行验证，我们需要将其做一些相对应的转换。由于我们采用了事务级的时序无关模型，所有的信号
  都被抽象掉，因此公式~(\ref{equ:safety})所表示的安全性以及公式~(\ref{equ:liveness})所表示的活性都应
  该被转换成与高抽象层次相对应的形式。具体来说，时序逻辑表达式中所设计到的信号都应该被转化成粗粒度的
  阶段(phase)，转化后的形式如下:

 \paragraph{安全性:}
  \begin{equation} \label{equ:trans_safety}
    \begin{split}
      \mathbf{G}!&((p1.phase == WRITE\ \&\ p2.phase == WRITE) \\
      &|\ (p1.phase == WRITE \ \&\ p2.phase == READ) \\
      &|\ (p1.phase == READ \ \&\ p2.phase == WRITE))
   \end{split}
  \end{equation}
  由于在抽象后的模型中所有的信号都已经被抽象掉，为了保证互斥读写，防止对于同一内存区域同时进行写写/
  读写操作，我们通过防止多个操作同时处于读/写阶段来做到这一点。例如，只要多个进程同时进入写阶段，无
  论其操作的内存地址是否相同，都会被认为是违反安全性的一个反例。很容易注意到很多相关细节在性质的转换
  过程中被丢弃了，这是因为在基于事务的时序无关模型中所有的信号都被抽象掉了。由此造成的问题就是性质的
  验证结果可能会不准确，这在前文中有所提及。

 \paragraph{活性}
  \begin{equation} \label{equ:trans_liveness}
    \begin{split}
      \mathbf{G}(&((p1.phase == COMMAND) \rightarrow \\
      & \qquad\qquad(p1.phase == WRITE\ |\ p1.phase == READ))\\
      \wedge &((p2.phase == COMMAND) \rightarrow \\
      & \qquad\qquad(p2.phase == WRITE | p2.phase == READ)))
    \end{split}
  \end{equation}
  很容易注意到，在该性质的转换过程中，几乎没有任何细节信息的损失。这是因为原始性
  质~(\ref{equ:liveness})中所设计到的信号都在模型的抽象过程中被分别映射到了不同的阶段(phase)中，因此
  该转换是简单而平滑的，只需要将对应的信号转换为其现在所属于的阶段就可以了。
\end{enumerate}

\begin{figure}[ht]
  \centering
  \includegraphics[scale=0.6]{un-timed}
  \caption{DTL-S协议时序无关模型的有限状态机}
  \label{fig:un-timed}
\end{figure} 

\subsubsection{模型检验和细化}
\label{sec:model_checking_refinement}
在基于事务的代验证模型以及相对应的待验证性质都已经准备完毕之后，我们就可以继续进行下一步的模型检验过
程。目前有很多高效的模型检验工具，比如说NuSMV\cite{DBLP:conf/cav/CimattiCGGPRST02}。NuSMV可以接受的
是smv格式的输入文件，而用以表示待验证模型的有限状态机FSM和表示待验证性质的时序逻辑可以很方便地转换成
smv格式，从而交给NuSMV求解，最终得到验证结果。

%TO-DO: 这里加上具体的转换算法吧，应该1-2天就可以完成。

以性质~(\ref{equ:trans_safety})和性质~(\ref{equ:trans_liveness})为例。对于性
质~(\ref{equ:trans_liveness})来说，由于在转换过程中并没有细节信息的丢失，因此基于事务级模型得到
的验证结果同样适用于寄存器传输级。但是对于性质~(\ref{equ:trans_safety})来说，由于信号$wr\_addr$和
$rd\_addr$在抽象后并不存在，在事务模型对该性质验证得到的结果并不一定等同于在寄存器传输级对原始性
质~(\ref{equ:safety})验证所得的结果。比如说，如果处理器$p1$写入地址$0x1000$，处理器$p2$写入地址
$0x2000$，这种情况对于性质~(\ref{equ:trans_liveness})来说是反例，因为$p1$和$p2$同时处于了$WRITE$阶
q1段；但是对于性质)~(\ref{equ:safety})来说，由于两者的$wr\_addr$信号值并不相同，实际上这并违反该性质所
表述的互斥写的安全性。

由于这种情况出现的可能性，在求解得到事务级模型的反例之后，我们可能需要做进一步的细化和再求解才能得出
最终的验证结果。这时，需要观察首先比对原始性质和抽象后的性质。如果两者相比仅仅是表现形式的差别，并没
有关键信息的不同(比如说关键信号在抽象后被掩盖)，如性质~(\ref{equ:liveness})和性
质~(\ref{equ:trans_liveness})，那么可以沿用高层的验证结论作为最终的结果；否则，如果在抽象过程中有关键
信息的丢失，例如性质~(\ref{equ:safety})和性质~(\ref{equ:trans_safety})，则要对高层次的模型做进一步的
细化，如图~\ref{fig:elaboration}所示。

\begin{figure}[hl]
  \centering
  \includegraphics[scale=0.6]{elaboration}
  \caption{细化后的有限状态机}
  \label{fig:elaboration}
\end{figure}

将图~\ref{fig:elaboration}和图~\ref{fig:un-timed}相比很容易看出，对于后者中的读阶段(read)、写阶段
(write)，前者在细化后分别划分成立了更小的两个阶段: $rd\_valid$, $rd\_accept$ 以及 $wr\_valid$,
$wr\_accept$，同时重新引入了读/写操作的地址信号$rd\_addr$和$wr\_addr$。这样就可以重新检验性
质~(\ref{equ:safety})是否存在反例。

有一点要注意的是，在上文中所描述的细化过程中，并不是所有的阶段(phase)都会被重新细化到寄存器传输级，
如图~\ref{fig:elaboration}中的命令(Command)阶段就并没有经过细化。实际上，当且仅当需要细化来验证相关
性质的时候，抽象后的模型才会转换到低抽象层次中。得益于此，即便经过细化，无论是状态空间还是问题规模都
要比时钟周期精确(Cycle-accurate)的事务级模型(TLM)要小，更不用说寄存器传输级模型了。这样的话，验证工
作量就会大大减小，而验证效率也会相应提高。

\subsection{对模型检验过程的改进}
\label{sec:improve_model_checking}

% TO-DO: 介绍NuSMV的工作流程
本文采用定界模型检验(Bounded Model Checking)技术来做最终的模型检验工作。在传统的定界模型检验流程中，
模型检验问题会被转换为可满足性(SAT)问题，最终交由布尔SAT求解器求解，并输出最终结果。对于寄存器传输级
(RTL)模型来说，由于其中包含大量的位运算以及布尔关系操作，利用布尔SAT求解器来求解无疑是一个比较恰当的
选择。但是一旦上升到更高的抽象层次，比如说事务级(Transaction Level)，这时代求解问题中的约束更多的已
经不是位级约束，而是诸如字级约束，线性规划问题等更高抽象层次的问题。这样一来，布尔SAT求解器无论在可
以接受的问题类型，以及在求解效率上都存在很大的局限性。

另外，在研究NuSMV的流程时，我们发现为了采用主流的布尔SAT求解器，在定界模型检验之前，NuSMV将待求解的
有限状态机转化为布尔编码。而如果我们能够采用支持复杂操作的求解器代替布尔SAT求解器，那么可接受输入的
问题形式就会灵活，同时也可以节省转化为布尔编码的时间。因此，我们决定采用可满足性模理论
(Satisfiability Module Theory, SMT)求解器来代替布尔SAT求解器。

% TO-DO: 介绍SMT求解器


\section{本章小结和展望}
\label{sec:conclude_hierarchy}

本章主要通过提出一种层次化形式验证方法，利用定界模型检验(BMV)技术，并借鉴抽象细化的思想，在验证效率和
验证完整性之间寻求一个折衷。在抽象层次低的寄存器传输级(RTL)可以保证验证的完整性，但其效率已经逐渐不能
满足日渐增长的设计规模；而在抽象层次高的事务级(TL)利用事务级模型(TLM)验证虽然可以提高验证效率，但对于
某些设计到具体型号的性质则无法保证其验证结果的完整性。利用层次化形式化验证方法，我们主要集中在事务级
做验证，然后在必要的时候对高层次模型做细化，降低到寄存器传输级做验证。由于并不是所有的性质都需要在寄
存器传输级做验证，因此这样可以在保证验证完整性的同时，尽可能地优化验证效率。但同时我们也仍然需要进一
步的实验数据的支撑来验证该方法在实际应用中的有效性。

\begin{itemize}
\item 层次化验证方法的效率严重依赖于待验证性质的特性，具体来说，取决于待验证性质的粒度及其分布。举例
  来说，如果所有的待验证性质都是时钟周期精确(cycle accurate)的，那么每一次得到最终的验证结果之前，我
  们都要将事务级模型细化到寄存器传输级模型。这样与直接在寄存器传输级做验证相比，不仅没有提高效率，反
  而要增加很多模型转换的开销。因此，我们需要对实际应用的验证过程中引入的待验证性质做进一步的分析，对
  层次化验证方法在实际应用中的作用做合理的评估。
\item 初步的实验结果显示，采用SMT求解器的定界模型检验过程的效率低于原始的NuSMV求解器。由于NuSMV自发
  布之初到现在已经经过多个版本的性能优化，对于该效率差异的具体原因需要进一步的分析。另外，我们也会进
  一步加入新的优化策略，比如说启发式的定界搜索策略。
\end{itemize}

\section{模型检验}
\label{sec:model-checking}

模型检验(Model Checking)在形式验证中占据非常重要的位置，也是近几十年以来形式验证最主要的发展力量。它
是由美国的Edmund M. Clarke 和 Allen Emerson\cite{WLP81_Clarke}，以及法国的Jean-Pierre
Queille 和 Joseph Sifakis\cite{EWATPN81_Queille}分别独立提出的。模型检验发展至今，不仅在软/硬件设计的
验证领域中占有极为重要的位置，此外在通信协议、安全算法的设计方面也发挥了很重要的作用。模型检验技术的
发明者Edmund M. Clarke，Allen Emerson和Joseph Sifakis三人也因为``在将模型检查发展为被软/硬件业中广泛
采用的高效验证技术上的贡献''被授予2007年度的图灵奖。

模型检验的主体思想是，首先将要验证的对象(比如说系统或者电子设计)抽象为有限状态机(Finite Sates
Machine)，待验证的性质则用时态逻辑(Temporal Logic)进行形式化的描述。由于待验证系统已经被抽象为有限状
态机，因此直观的想法就是如果我们遍历状态机中的每个状态，同时查看性质$P$在该状态是否成立，就可以判断在
整个状态空间中是否存在违反该性质$P$的反例，从而得出结论。因此模型检验的过程一般是三段式的，包括系统
建模、性质形式化表示以及验证。

模型检验相对于定理证明来说，由于实现方式和理论基础都相对要简单很多，给验证工作的进行带来了很大的便
利，也因此引领了形式验证技术的发展。但模型检验技术也并不是形式验证领域的``银弹''，它同样有自己的瓶颈。
正如上文提到的，模型检验虽然可以实现验证工作的自动化完成，实际上是通过遍历有限状态机的状态空间来判断
性质是否满足的，这样对于规模大的问题就不可避免地遇到状态空间爆炸的问题。实际上这也正是模型检验技术从
开创至今一直努力克服的问题，模型检验发展的历史，实际上就是在克服空间爆炸问题的道路上不断摸索前进的过
程。

模型检验技术发展至今，按照时间先后分别出现了显式模型检验，符号模型检验(Symbolic Model Checking)和
定界模型检验(Bounded Model Checking)三种。

\paragraph{显式模型检验}
显式模型检验就是上文中提到的显式遍历状态机状态空间的方法。

\paragraph{符号模型检验}
符号模型检验(SMV)是由K.L. Mcmillan将Randal E. Bryant提出的的有序二叉判别图(Ordered Binary
Decision Diagram，OBDD)应用于模型检验技术中，提出的一种新型的检验方法。由于OBDD可以表示状态组而不是
单个状态之间的转换关系，状态空间爆炸的问题得到很大的缓解，模型检验能够处理的问题规模有了很大的提高。
也是从符号模型检验SMV开始，模型检验技术开始走出学院，广泛应用于工业界，并获得了巨大的成功。

\paragraph{定界模型检验}
对于二叉判别图BDD来说，由于要进行状态穷举遍历，每个变量的两种取值可能(0和1)都要表现出来，因此未经化
简的BDD是一个完全二叉树，其规模与变量数呈指数关系。虽然通过多种手段对其进行化简，但存储和操作BDD仍然
需要很大的空间。因此，在定界模型检验SMV之后，Armin Biere于1999年提出了定界模型检验
(BMV)\cite{Biere03boundedmodel}。定界模型检验是基于可满足性(Satisfiability, SAT)问题提出的一种模型检
验方法。它的基本思想是将模型检验问题转化为一个可满足性问题，并借助于SAT求解器来得出结果。具体来讲，
定界模型检验会将待验证性质$P$取反得到$\neg P$，并给定一个界限$k$，将有限状态机$M$展开$k$个时序，并和待验证性质
$P$结合构成一个可满足性(SAT)问题。如果求解得知该问题满足，即原始设计在$k$个时序内满足性质$\neg P$，就说明
我们已经找到了性质$P$的一个反例。否则的话，我们需要继续提高$k$，或者在到达预定的最大上限后认为反例无
法找到。

相对于采用BDD的符号模型检验来说，由于不需要保存BDD，基于SAT问题的定界模型检验最大的优势是不存在空间爆
炸问题。而且虽然SAT问题是NP-Complete问题，但是在实际应用中仍然非常有效。而且得益于近几年SAT求解技术
的蓬勃发展，定界模型检验的效率以及可以处理的问题规模也有很大的提高。

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "../main"
%%% End: 
